\begin{tabbing}
$M$:$k$ may not read $x$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$x$ $\in$ dom(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of($M$))))))))))))\+
\\[0ex]$\wedge_{2}$ $\neg_{2}$deq{-}member(KindDeq;$k$;1of(\=2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(\+
\\[0ex]$M$)))))))))))($x$))
\-\-
\end{tabbing}